
% A rule inside a tabular. 1: name, 2: arrow, 3 and 4: before and after the arrow (upper)
% 5 and 6:  before and after the arrow (upper)
\newcommand{\myrule}[6]{\mbox{\textsc{#1}}~~ {\displaystyle \frac{#3 #2 #4}{#5 #2 #6}}}

% A rule inside a tabular (basic version). 1: name, 2: upper the line, 3: below the line
\newcommand{\mybasicrule}[3]{\mbox{\textsc{#1}}~~ {\displaystyle \frac{#2}{#3}}}

% An axiom (without a line) inside a tabular. 1: name, 2: arrow, 3 and 4: before and after the arrow (below)
\newcommand{\myaxiom}[4]{\mbox{\textsc{#1}}~~ {\displaystyle {#3 #2 #4}}}

% I am too lazy for doing angular parenthesis
\newcommand{\angp}[1]{\ensuremath{\langle #1 \rangle}}

% The classic encoding notation. The second parameter serves to 'decorate' it.
\newcommand{\os}{[\![}
\newcommand{\cs}{]\!]}
\newcommand{\encp}[2]{\os #1 \cs_{#2}}



% Encoding of numbers for the MM encoding:
\newcommand{\on}{(\!|}
\newcommand{\cn}{|\!)}
\newcommand{\encn}[2]{\on #1 \cn_{#2}}
\newcommand{\encu}[1]{\on #1 \cn}

% This is used for the proof of correctness of the encoding of MM
%\newcommand{\obj}[3]{\ensuremath{\mathcal{#1}^{\,#2}_{\,#3}}}

% Match command for CCS
\newcommand{\match}[3]{\ensuremath{\mathsf{match}\, #2 = #1\, \mathsf{in}\, #3}}
%\newcommand{\ifthen}[3]{\ensuremath{\mathsf{if}\, #1\,\mathsf{then}\, #2\, \mathsf{else}\, #3}}

\renewcommand{\ts}[1]{\textsc{#1}}

% Abbreviations for languages and encodings
\newcommand{\hopi}{\ensuremath{\textsc{HO}\pi}\xspace}
\newcommand{\ccsv}{\ensuremath{\textsc{CCS}_\mathcal{V}}\xspace}
\newcommand{\inrep}{\ensuremath{\mathsf{i}!}}
\newcommand{\mms}{\ensuremath{\mathsf{M}}}
\newcommand{\cho}{\ensuremath{+}}

% Abbreviations for bisimulations
\newcommand{\io}{\textsc{IO}\xspace}
\newcommand{\ios}{\ensuremath{\sim_{\mathrm{\io}}}\xspace}
\newcommand{\ho}{\textsc{HO}\xspace}
\newcommand{\hos}{\ensuremath{\sim_{\mathrm{\ho}}}\xspace}

% Trigger
\newcommand{\trigger}[1]{\ensuremath{\overline{#1}}\xspace}

% I am lazy writing substitutions
\newcommand{\subst}[2]{\ensuremath{\{#1/#2\}}}

% Some relations
\newcommand{\stcon}[1]{\ensuremath{\equiv_{{#1}}}}

% This is for writing optional content. The first parameter will appear in the long version, 
% and the second one in the short one.
\newcommand{\iflong}[2]{\ifthenelse{\boolean{lversion}}{#1}{#2}}

% Titles for theorems, definitions and the like.
%\newtheorem{definition}{Definition}[section]

\newtheorem{mydefi}[definition]{Definition}
\newtheorem{myrem}[definition]{Remark}
\newtheorem{myconv}{Convention}[definition]
\newtheorem{mytheo}[definition]{Theorem}
\newtheorem{mylem}[definition]{Lemma}
\newtheorem{myprop}[definition]{Proposition}
\newtheorem{mycoro}[definition]{Corollary}
\newtheorem{myexam}[definition]{Example}
\newtheorem{miprop}[definition]{Proposition}


%\newtheorem{example}[definition]{Example}
%\newtheorem{lemma}[definition]{Lemma}
%\newtheorem{theorem}[definition]{Theorem}
%\newtheorem{corollary}[definition]{Corollary}
%\newtheorem{proposition}[definition]{Proposition} 
%\newtheorem{remark}[definition]{Remark}
\newtheorem{newnotation}[theorem]{Notation}
%\newtheorem*{lemma2}{Lemma}
%\newtheorem*{corollary2}{Corollary}
%\newtheorem*{theorem2}{Theorem}

\newcommand{\mydef}{\ensuremath{\stackrel{\mathrm{def}}{=}}}

\newcommand{\msend}[2]{\overline{#1}\langle #2 \rangle}
\newcommand{\pired}{\longrightarrow}
\newcommand{\notpired}{\nrightarrow}
\newcommand{\divpired}{\Uparrow}
\newcommand{\minskred}{\longrightarrow_{\textrm{\textsc{M}}}}
\newcommand{\notminskred}{\nrightarrow_{\textrm{\textsc{M}}}}
\newcommand{\divminskred}{\Uparrow_{\textrm{\textsc{M}}}}

\newcommand{\choice}[1]{\widehat{#1}}

\newcommand{\regzeroname}[1]{r^{0}_{#1}}
\newcommand{\regsuccname}[1]{r^{\mathsf{S}}_{#1}}
\newcommand{\regzero}[1]{\overline{\regzeroname{#1}}}
\newcommand{\regsucc}[2]{\overline{\regsuccname{#1}}\angp{#2}}
\newcommand{\rz}[1]{\choice{z_{#1}}}
\newcommand{\rnz}[1]{\choice{n_{#1}}}
\newcommand{\size}[1]{\#(#1)}
\newcommand{\sizet}[1]{\mathbf{size}(#1)}
\newcommand{\rewrite}{\ensuremath{\leadsto}}
\newcommand{\nf}[1]{\ccc{n}(#1)}


\newcommand{\DIS}{{\tt DIS}}
\newcommand{\ext}{\mathrel{\equiv_{\tt E}}}
\newcommand{\Bigpi}[3]{\Pi_{#1}^{#2}\: #3}

\newcommand{\co}[1]{\overline{#1}}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

% Comments
\newboolean{draft}
\newcommand{\comment}[2]{\ifdraft{[\emph{\textbf{#1:} #2}]\fi}}
\newcommand{\finish}[1]{\comment{FINISH}{#1}}
\newcommand{\as}[1]{\comment{AS}{#1}}
\newcommand{\changed}{\comment{CHANGED}{}}
